Lambda the Ultimate

Ran across a short weblog entry on Leonhard Euler, the father of functions and initiator of much in the way of number theory. The mention of Project Euler caught my eye, as I rather like projects that involve multiple PLs attacking the same sets of problems.

Project Euler is a series of challenging mathematical/computer programming problems that will require more than just mathematical insights to solve. Although mathematics will help you arrive at elegant and efficient methods, the use of a computer and programming skills will be required to solve most problems. The motivation for starting Project Euler, and its continuation, is to provide a platform for the inquiring mind to delve into unfamiliar areas and learn new concepts in a fun and recreational context.

Project Euler has been around for almost as long as LtU but this is the first I'd heard of it. I find the questions and the competitive gaming aspect to be interesting, though I have a long way to go (level 2 out 5). Not sure there is a direct tie into PLs, but since I'm using it to learn more math and investigate the breaking points and elegance of PLs... and anything involving multiple PLs in competition and mathematics can't be too far removed... and since I haven't posted a story to LtU in a while and this happens to be my current interest... well, that will have to suffice. I'll have to admit though that many of the solutions I looked at are either too rushed (brute force), too cumbersome (indexes flying everywhere) or too terse. But that's true of most code that I run across (including my own). Still hoping for a PL that has that just right aspect - though I'm leaning to Oz these days.

_{(For those of us that are looking for walk-through/cheat guides, the Haskell wiki has the code to the first 200 problems, and I've put my Oz code for the first 50 up on the CTM wiki).}

The notes from a panel held at POPL 2009 on this topic are available here.
The panelists were Simon Peyton Jones, Kathryn McKinley, Xavier Leroy, Martin Rinard and Greg Morrisett.

Among the topics raised: Effects, Program verification, Parallelism, Visualization tools for understanding behavior of parallel programs, Secure software, High assurance.

Not surprisingly all these topics have been discussed here repeatedly in recent years...

(seen via http://catless.ncl.ac.uk/Risks/25.51.html#subj9.1, i didn't find it searching on ltu yet)

at qcon, london:

Abstract: I call it my billion-dollar mistake. It was the invention of the null reference in 1965. At that time, I was designing the first comprehensive type system for references in an object oriented language (ALGOL W). My goal was to ensure that all use of references should be absolutely safe, with checking performed automatically by the compiler. But I couldn't resist the temptation to put in a null reference, simply because it was so easy to implement. This has led to innumerable errors, vulnerabilities, and system crashes, which have probably caused a billion dollars of pain and damage in the last forty years. In recent years, a number of program analysers like PREfix and PREfast in Microsoft have been used to check references, and give warnings if there is a risk they may be non-null. More recent programming languages like Spec# have introduced declarations for non-null references. This is the solution, which I rejected in 1965.

Phil Windley posted a few useful links about this topic following WWW2008.

Bonus question: How is this item connected to the one I posted earlier today?

McCarthy's Elephant language proposal was mentioned here several times in the past. This talk from Etech provides a nice introduction to the fundamental idea behind Elephant and its background.

The talk includes interesting, though not entirely motivated, comments related to the paper Ascribing Mental Qualities to Machines. This is one of McCarthy's most significant papers in my opinion, and deserves more attention and debate. It is also rather amusing. I hope I will find the time some day to put this paper in context (McCarthy's comments in the Etech talk notwithstanding), but for the time being I recommend it to anyone interested in this sort of thing.

One thing is for sure: We can safely add to the 2009 predictions the prediction that Elephant will not be ready in 2009...

Ziggurat is a framework for writing extensible programming languages, and for defining static semantics for those languages. In other words, it is a language designer's toolkit.

Ziggurat is based on macros. When building a language using Ziggurat, it is easy to make that language extensible by adding a macro system. Ziggurat macros allow for incremental extension of the language by rewriting. What makes Ziggurat different from other macro systems is that Ziggurat allows the language extender to optionally define static semantics for her new language, and connect these static semantics amongst language levels. This makes it possible to write specialized analysis algorithms for the higher-level languages, either for optimization purposes, profiling purposes, debugging purposes, or whatever task analysis is put to.

Strangely enough this project from Olin Shivers and David Fisher was not mentioned here before.

Those with access may want to check out the paper on Ziggurat in the September 2008 double issue of JFP.

Path Feasibility Analysis for String-Manipulating Programs. Nikolaj Bjorner, Nikolai Tillmann, Andrei Voronkov.

We discuss the problem of path feasibility for programs manipulating strings using a collection of standard string library functions. We prove results on the complexity of this problem, including its undecidability in the general case and decidability of some special cases. In the context of test-case generation, we are interested in an efficient finite model finding method for string constraints. To this end we develop a two-tier finite model finding procedure. First, an integer abstraction of string constraints are passed to an SMT (Satisfiability Modulo Theories) solver. The abstraction is either unsatisfiable, or the solver produces a model that fixes lengths of enough strings to reduce the entire problem to be finite domain. The resulting fixed-length string constraints are then solved in a second phase. We implemented the procedure in a symbolic execution framework, report on the encouraging results and discuss directions for improving the method further.

The authors note that while strings are a fundamental data type, the main existing way of handling strings in symbolic test-case generation tools is to treat them as regular arrays, and to treat string library subroutines as regular procedure calls, thus turning even simple calls to library functions into loop constructs.

Benjamin Werner explore a type theory that, among other things, might be a first step towards making a proof assistant that's also a more traditional programming environment in On the Strength of Proof-Irrelevant Type Theories, Logical Methods In Computing 2008.

Abstract. We present a type theory with some proof-irrelevance built into the conversion rule. We argue that this feature is useful when type theory is used as the logical formalism underlying a theorem prover. We also show a close relation with the subset types of the theory of PVS. We show that in these theories, because of the additional extentionality, the axiom of choice implies the decidability of equality, that is, almost classical logic. Finally we describe a simple set-theoretic semantics.

A suggested application lies a few paragraphs in.

In order to identify more terms it thus is tempting to [integrate] program extraction into the formalism so that the conversion rule does not require the computationally irrelevant parts of terms to be convertible.

In what follows, we present and argue in favor of a type-theory along this line. More precisely, we claim that such a feature is useful in at least two respects. For one, it gives a more comfortable type theory, especially in the way it handles equality. Furthermore it is a good starting point to build a platform for programming with dependent types, that is to use the theorem prover also as a programming environment. ...

Guido van Rossum is recounting the history of Python as a series of blogposts. It's off to a good start.
http://python-history.blogspot.com/

In the history of PL design there has been quite a bit of vitriol spilled over design choices. These days bringing up "static vs dynamic typing" is a good way to generate some heat on a cold winter web forum.

But a few debates seem to have been pretty firmly resolved, at least for general purpose languages. GP languages have considered goto harmful for decades now, dynamic scoping is seen as a real oddity, and manual memory management is a choice only made by systems language designers.

Questions for LtU: What other debates have been "resolved" in the sense that general purpose languages are hardly ever designed with an alternative to the consensus? What debates will be resolved in the near future? And what apparently resolved debates deserve to be reopened?

One rule: "static vs dynamic typing" will be considered off topic because clearly and emphatically that debate hasn't been resolved and has no prospect of being resolved any time soon. Also, it's boring.